package systemf



class Context(bindings: List[(String,Binding)]){
  
 object debruijn extends DeBruijnSubstitution
 import debruijn.addingBinder
 
 type VarRef= Int
 private val bins : List[(String,Binding)] = bindings
 

 
 def apply(i: VarRef) : Option[Binding]  = if (!(0<=i && i < bins.length)) None else {
       bins(i)._2 match { 

   case VarBinding(ty) => {
     
//   CAREFUL: why typeshift: suppose we are looking up var(0), declared in the lambda(= _outside of body_ of lambda) as tyvar(0). we are now looking it up from within, so we expect to see it as tyvar(1), because 0 is now our inner lambda var instead of the outer type binding
     //Some(VarBinding(typeShift(i+1,ty)).asInstanceOf[A])
     var tymod = ty     
     for (_ <- List.range(0,i+1)) {tymod = addingBinder(tymod)} //do i+1 times
     Some(VarBinding(tymod))
   }
   case b@_            => 
     Some(b)
 }} 
 
 def + (n: String, b: Binding) = new Context ( (n,b):: bins) 
 
 
 def getIndexOfName(n: String) :VarRef = getIndexOfName(n, bins)
 private def getIndexOfName(n: String,bins: List[(String,Binding)]) : Int = {
   val index = bins.map {case (n, _) => n} indexOf(n)
   if(index == -1) throw new Exception(n +" is unbound variable") else index
 }
   
 def isNameBound(n: String): Boolean =  bins exists { case (s, b)  => (s == n) }
 
 
   
 def pickDisplayName(n: String) :(Context,String)= {
    if (isNameBound(n)) pickDisplayName(n+"'")
    else (this + (n, NameBinding(n)), n)
 }

 def pickDisplayNameType(n: String) :(Context,String) = {
    if (isNameBound(n)) pickDisplayNameType(n+"'")
    else (this + (n, TypeVarBinding(n)), n)
 }
   
   
   
   
 override def toString = bins.toString
 
}
 abstract class Binding 
 case class NameBinding(name: String) extends Binding 
 case class VarBinding(ltype: LType) extends Binding 
 case class TypeVarBinding(name: String) extends Binding 

 




